#define USERS	2
/* Bidder1 States */

mtype = {idleB, startB, submittedB};

/* Auctioneer States */

mtype ={waitA, startA, processBidA, endA};

/* Events*/

mtype = {start_auction, auction_started, status, winner, loser, end_auction, dummy, send_bid, danger, paying};

mtype stateA;
bool dang = false;

/* channels for transitions */	

int amountOfClients = USERS;
int startBid=0;

chan m2A = [0] of {int, mtype};
chan m2B[USERS] = [1] of {int, mtype};

/* Winning client */
int clientId;
int clientBid;

/* Stuff for LTL */
bool someoneWon = false;
int amountOfBids = 0;
int bids[USERS];
int max_id = -1;
int round = 0;

init {
    int i = 0;
    do
    :: (i<amountOfClients) -> run client(i);
        i = i+1;
    :: (i==amountOfClients) -> break;
    od;
    run auctioneer();
    m2A!0, start_auction;
    printf("Msg to start the auction\n");
}

/*Client process*/

proctype client(int id) {
    mtype stateB = idleB;
    int bid;
    atomic {
	if
	:: skip -> bid = 5;
	:: skip -> bid = 6;
	:: skip -> bid = 7;
	fi;
    }
    
    do
    :: m2B[id]?0, auction_started ->
        printf("The auction is now open, the client %d knows",id);
    :: m2B[id]?0, end_auction -> printf("Auction is terminating \n");
        break;
    :: m2B[id]?0,send_bid -> printf("Ready to submit a bid\n");
        printf("Sending bid \n");
        m2A!bid, dummy; bids[id] = bid;
        stateB = submittedB;
        printf("Bid submitted\n");
    ::m2B[id]?bid, winner->
        printf("Hurray, I won\n");
        m2A!bid,paying;
        stateB = idleB;
    ::m2B[id]?0, loser ->
        printf("I lost :(\n");
        stateB = idleB;
    ::m2B[id]?0, danger ->
        printf("Auction Shutdown\n");
	break;
    od;
}


/*Auction process*/

proctype auctioneer() {
    int max_bid = startBid;
    int i = 0;
    stateA = waitA;
    int bid;
    int id;
    do
    :: (id<amountOfClients && stateA!=endA) ->
        do 
        :: dang ->
            do
            :: (i<amountOfClients) -> m2B[i]!0,danger;i = i + 1;
            :: (i==amountOfClients) -> i = 0; break;
            od;
        :: (stateA == waitA && !dang) -> printf("Waiting to start the auction\n");
            m2A?0, start_auction;
            printf("Ready to get the auction started\n");
            do
            :: (i<amountOfClients) -> m2B[i]!0,auction_started;
                i = i+1;
            :: (i==amountOfClients) -> i = 0;
                break;
            od;
            stateA = startA;
            printf("Sending start signal\n");
        :: (stateA == startA && !dang) -> printf("Should Player %d submit a bid\n",id);
            if
            :: max_id==id -> break;
            :: else -> skip;
            fi;
           m2B[id]!0,send_bid;
            printf("Waiting for a bid to be submitted by %d....\n",id);
            m2A?bid, dummy;
            amountOfBids=amountOfBids+1;
            printf("Client bid received\n");
            stateA=processBidA;
        :: (stateA == processBidA && !dang) -> printf("Computing if it is winning bid\n");
            if
            :: bid != -1 && bid>max_bid -> max_bid = bid; max_id = id;
            :: bid != -1 && bid==max_bid -> max_id = -1;
            :: bid != -1 && bid<max_bid -> skip;
            fi;
            stateA = startA;
            break;
        od;
        id = id + 1;
    :: (id==amountOfClients && stateA!=endA) -> 
        round = round + 1;
        max_bid = max_bid + 1; id = 0;printf("NEW ROUND: %d \n",round);
        stateA = endA;
    :: (stateA==endA) -> 
        printf("Winner elected.Auction will terminate\n");
        do
        :: (i<amountOfClients && i==max_id) -> 
            m2B[i]!(max_bid-1),winner;
            m2A?max_bid,paying;
            printf("Winner paid %d",max_bid);
            someoneWon = true;
            m2B[i]!0,end_auction;
            i = i+1;
        :: (i<amountOfClients && i!=max_id) -> 
            m2B[i]!0,loser;
            m2B[i]!0,end_auction;
            i = i + 1;
        :: (i==amountOfClients) -> i = 0; break;
        od;
        break;
    od;
    printf("Shutting down auctioneer\n");
}

//ltl   i {[] (round<2) }
//ltl  ii {!someoneWon U (amountOfBids == amountOfClients)}
ltl iii {[] ((amountOfBids<amountOfClients) -> !someoneWon)}
